package ch.epfl.lara.matcheck.verify;

/**
 * <b> Abstract Formula Maker </b> 
 *    <p>
 *    	Is a simple trait that encapsulate methods useful to transform:
 *	<ul>
 *	   <li> Connect a list of propositions/atoms using binary logic connectors as '&', '|', ...</li>
 *	   <li> List of sets into a formula (in set logic). </li>
 *	</ul>
 *   </p>
 */
trait AbstractFormulaMaker {
   
  /** <b> Conjuncted formula.</b>
   *   <p> 
   *      Create a formula that is a conjunction of the atoms passed in parameter. 
   *  </p>
   *
   * @parameter and     : The conjunctive binary or operator.
   * @parameter atoms   : The list of atoms. 
   * @return            : The conjuncted formula.
   */
  protected def conjunction[T](basecase: T, and: (T,T) => T)(atoms: List[T]): T = 
    connectAtoms(basecase)(and)(atoms)
   
   
   
  /** <b>Disjunctive formula.</b>
   *   <p> 
   *      Create a formula that is a disjunction of the atoms passed in parameter. 
   *  </p>
   *
   * @parameter or      : The disjunctive binary or operator.
   * @parameter atoms   : The list of atoms. 
   * @return            : The disjuncted formula.
   */
  protected def disjunction[T](basecase: T, or: (T,T) => T)(atoms: List[T]): T = 
    connectAtoms(basecase)(or)(atoms)
  
  
  
  /**
   *   <p> 
   *     Create a formula that use the binary connector operator gave in argument
   *	 between any two atoms.  
   *  </p>
   *
   * @parameter operator    : The binary operator. 
   * @parameter propositions: The list of atoms.
   * @return                : The formula. 
   */
  private def connectAtoms[T](basecase: T)(connector: (T,T) => T)(atoms: List[T]): T = {
    (atoms.:\ (basecase)) {
      (atom,acc) => connector(atom,acc)
    }
  }
  
  
   
  /**
   * <p>
   *	Create a formula that use a binary connector that does not belong to the first order logic
   *	theory ('&','|'). Hence, no basecase exists for such general connector and the list
   *	of elements is required to contain at least one element.
   * </p>
   *
   * @param connector: The binary connector operator. 
   * @param elements : The list of elements. 
   * @return         : A formula with the connector applied between any two atoms.
   *
   * precondition: elements.size() > 0
   */
  protected def connectElements[T](connector: (T,T) => T)(elements: List[T]): T = elements match {
    case Nil => error("Two elements are necessary to infix a binary operator")
    case e :: Nil => e
    case many => 
      many.reduceLeft[T]((left,right) => connector(left,right))
  }
  
  
}
